\begin{tabbing}
weakSendDoApplyR\=\{\$a:ut2, \$tg:ut2\}\+
\\[0ex]($T$; $t$; $l$; ${\it ds}$; $f$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$weakPrecondSendR2\=\{\$a:ut2, \$tg:ut2\}\+
\\[0ex]($T$; $t$; $\ast$1$\ast$; $l$; ${\it ds}$; ($\lambda$$s$.can{-}apply($f$;$s$)); ($\lambda$$s$,$v$. do{-}apply($f$;$s$)))
\-
\end{tabbing}